(declare-fun a () Real)
(declare-fun b () Real)
(assert (< b 0.2))
(assert (= 1 (- b a)))
(assert (or (> b 0) (= 1 (/ 1 b))))
(check-sat)
(push)
(check-sat)
(pop)
(assert (= a 1))
(check-sat)
